I would like an informal discussion of the theorem prover.  It sounds
like an advance all right.  Apart from that, Cartwright's thesis gets
total correctness of LISP nicely into first order logic, and I have
an extension of his results that put proving non-termination into the
same framework as well as what I think is a slight cleanup of his
results.  My ideas concern the logical formalism - not heuristics,
but now for the first time, I understand a good first order theory of
partial functions.  I do not exclude the possibility that others have
understood it previously.

	Cartwright is here for a week or so, and we should meet while
he is here.